MsgA(ds;da)
== x:Id fp ds(x)?Void
== a:Id fp State(ds)Valtype(da;locl(a))Prop
== kx:KndId fp State(ds)Valtype(da;1of(kx))ds(2of(kx))?Void
== kl:KndIdLnk fp (tg:Id(State(ds)Valtype(da;1of(kl))(da(rcv(2of(kl),tg))?Void List))) List
== x:Id fp Knd List
== ltg:IdLnkId fp Knd List
== k:Knd fp Id List
== k:Knd fp IdLnk List
== ltg:Id fp Knd List
== Top 

latex

---

clarification:

msga-body{i:l}
msga-body(ds; da)
== x:Id fp fpf-cap(ds;IdDeq;x;Void)
== a:Id fp State(ds)Valtype(da;locl(a))Prop{i}
== kx:KndId fp State(ds)Valtype(da;1of(kx))fpf-cap(ds;IdDeq;2of(kx);Void)
== kl:KndIdLnk fp
== (tg:Id(State(ds)Valtype(da;1of(kl))(fpf-cap(da;KindDeq;rcv(2of(kl),tg);Void) List))) List
== x:Id fp Knd List
== ltg:IdLnkId fp Knd List
== k:Knd fp Id List
== k:Knd fp IdLnk List
== ltg:Id fp Knd List
== Top 

latex

Definitions	locl(a), Prop, IdDeq, State(ds), x:AB(x), Valtype(da;k), 1of(t), f(x)?z, KindDeq, rcv(l,tg), 2of(t), Void, IdLnk, x:AB(x), a:A fp B(a), Id, type List, Knd, Top
FDL editor aliases	msga-body